perm filename BLISET.COM[226,JMC] blob sn#005395 filedate 1972-06-18 generic text, type T, neo UTF8
(GIVEAX EQ1 ((FORALL X) (EQUAL X X)))

(GIVEAX EQ2
 ((FORALL X) ((FORALL Y) (IMPLIES (EQUAL X Y) (EQUAL Y X)))))

(GIVEAX EQ3
 ((FORALL X)
  ((FORALL Y)
   ((FORALL Z)
    (IMPLIES (AND (EQUAL X Y) (EQUAL Y Z)) (EQUAL X Z))))))

(GIVEAX TABLEEMPTY
 ((FORALL X)
  (IMPLIES
   (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S0)))
   (NOT (AT X TABLE S0)))))

(GIVEAX DIFFOBJ
 (AND
  (NOT (EQUAL BOX1 BOX2))
  (AND
   (NOT (EQUAL BOX1 TABLE))
   (AND
    (NOT (EQUAL BOX1 DOOR))
    (AND
     (NOT (EQUAL BOX1 OUTSIDE))
     (AND
      (NOT (EQUAL BOX2 TABLE))
      (AND
       (NOT (EQUAL BOX2 DOOR))
       (AND
	(NOT (EQUAL BOX2 OUTSIDE))
	(AND
	 (NOT (EQUAL TABLE DOOR))
	 (AND
	  (NOT (EQUAL TABLE OUTSIDE))
	  (NOT (EQUAL DOOR OUTSIDE))))))))))))

(GIVEAX ATONE
 ((FORALL X)
  ((FORALL P1)
   ((FORALL P2)
    ((FORALL S)
     (IMPLIES (AND (AT X P1 S) (AT X P2 S)) (EQUAL P1 P2)))))))

(GIVEAX REDDOOR
 ((THEREEXISTS X)
  (AND
   (RED X)
   (AND
    (NOT (EQUAL X ROBOT))
    (AND
     (AT X DOOR S0)
     ((FORALL Y)
      (IMPLIES
       (AND
	(AT Y DOOR S0)
	(AND (NOT (EQUAL Y ROBOT)) (NOT (HOLDING Y S0))))
       (RED Y))))))))

(GIVEAX ISKEYBOX (OR (EQUAL KEYBOX BOX1) (EQUAL KEYBOX BOX2)))

(GIVEAX KEYBOX1
 ((THEREEXISTS X)
  (AND
   (KEY X)
   (AND
    (NOT (EQUAL X ROBOT))
    (AND (AT X KEYBOX S0) (NOT (HOLDING X S0)))))))

(GIVEAX KEYBOX2
 ((FORALL Y)
  (IMPLIES
   (AND
    (AT Y KEYBOX S0)
    (AND (NOT (EQUAL Y ROBOT)) (NOT (HOLDING Y S0))))
   (KEY Y))))

(GIVEAX B1B2 (NOT (EQUAL BOX1 BOX2)))

(GIVEAX B1T (NOT (EQUAL BOX1 TABLE)))

(GIVEAX B1D (NOT (EQUAL BOX1 DOOR)))

(GIVEAX B1O (NOT (EQUAL BOX1 OUTSIDE)))

(GIVEAX B2T (NOT (EQUAL BOX2 TABLE)))

(GIVEAX B2D (NOT (EQUAL BOX2 DOOR)))

(GIVEAX B2O (NOT (EQUAL BOX2 OUTSIDE)))

(GIVEAX TD (NOT (EQUAL TABLE DOOR)))

(GIVEAX TO (NOT (EQUAL TABLE OUTSIDE)))

(GIVEAX DO (NOT (EQUAL DOOR OUTSIDE)))

(GIVEAX HOLDING
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y)
    (IMPLIES (AND (AT ROBOT Y S) (HOLDING X S)) (AT X Y S))))))

(GIVEAX HOLD2
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y)
    (IMPLIES (AND (HOLDING X S) (HOLDING Y S)) (EQUAL X Y))))))

(GIVEAX PICKUP
 ((FORALL S)
  ((AND
    ((LAMBDA SP)
     ((FORALL X) ((FORALL Y) (EQUIVALENT (AT X Y S) (AT X Y SP)))))
    ((FORALL Z)
     (IMPLIES
      (AND
       (AT ROBOT Z S)
       ((THEREEXISTS X) (AND (NOT (EQUAL X ROBOT)) (AT X Z S))))
      ((THEREEXISTS X) (HOLDING X SP)))))
   (PICKUP S))))

(GIVEAX GO1
 ((FORALL S)
  ((FORALL Z)
   ((FORALL W)
    (EQUIVALENT (HOLDING W S) (HOLDING W (GOO Z S)))))))

(GIVEAX GO2
 ((FORALL S)
  ((FORALL Z)
   (IMPLIES
    (OR
     (NOT (EQUAL Z OUTSIDE))
     ((THEREEXISTS X) (AND (AT X DOOR S) (KEY X))))
    (AT ROBOT Z (GOO Z S))))))

(GIVEAX GO3
 ((FORALL S)
  ((FORALL Z)
   ((FORALL X)
    ((FORALL Y)
     (IMPLIES
      (AND
       (AT X Y S)
       (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S))))
      (AT X Y (GOO Z S))))))))

(GIVEAX GO4
 (IMPLIES
  (AND
   ((FORALL S)
    ((FORALL Y) ((FORALL X) (NOT (AND (AT X DOOR S) (KEY X))))))
   (AT ROBOT Y S))
  (AT ROBOT Y (GOO OUTSIDE S))))

(GIVEAX GO5
 ((FORALL S)
  ((FORALL Z)
   ((FORALL X)
    ((FORALL Y)
     (IMPLIES
      (AND
       (NOT (EQUAL X ROBOT))
       (AND (NOT (HOLDING X S)) (AT X Y (GOO Z S))))
      (AT X Y S)))))))

(GIVEAX RELEASE1
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y) (EQUIVALENT (AT X Y S) (AT X Y (RELEASE S)))))))

(GIVEAX RELEASE2
 ((FORALL S) ((FORALL X) (NOT (HOLDING X (RELEASE S))))))

(GIVEAX SITDEF
 ((FORALL S)
  ((FORALL Y)
   ((FORALL X)
    (EQUIVALENT (MEMBER X (SIT Y S)) (SITTING X Y S))))))

(GIVEAX SITSET ((FORALL S) ((FORALL Y) (ISSET (SIT Y S)))))

(GIVEAX EXTENSIONALITY
 ((FORALL U)
  ((FORALL V)
   (IMPLIES
    (AND (ISSET U) (ISSET V))
    (IMPLIES
     ((FORALL X) (EQUIVALENT (MEMBER X U) (MEMBER X V)))
     (EQUAL U V))))))

(GIVEAX SITTING
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y)
    (EQUIVALENT
     (SITTING X Y S)
     (AND
      (AT X Y S)
      (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S)))))))))


(PROOF ONE) 
1 	(USEAX SITDEF S Y X)
2 	(USEAX SITDEF (GOO Z S) Y X)
3 	(USEAX SITTING S X Y)
4 	(USEAX SITTING (GOO Z S) X Y)
5 	(USEAX GO1 S Z X)
6 	(USEAX GO3 S Z X Y)
7 	(USEAX GO5 S Z X Y)
8 	(TAUT
	 (EQUIVALENT
	  (MEMBER X (SIT Y S))
	  (MEMBER X (SIT Y (GOO Z S))))
	 1
	 2
	 3
	 4
	 5
	 6
	 7)
9 	(UG 8 X)
10 	(USEAX SITSET S Y)
11 	(USEAX SITSET (GOO Z S) Y)
12 	(USEAX EXTENSIONALITY (SIT Y S) (SIT Y (GOO Z S)))
13 	(TAUT (EQUAL (SIT Y S) (SIT Y (GOO Z S))) 9 10 11 12)
14 	(UG 13 S Y)